1  /-
  2  Copyright (c) 2017 Microsoft Corporation. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Parallel computation of a computable sequence of computations by
  7  a diagonal enumeration.
  8  The important theorems of this operation are proven as
  9  terminates_parallel and exists_of_mem_parallel.
 10  (This operation is nondeterministic in the sense that it does not
 11  honor sequence equivalence (irrelevance of computation time).)
 12  -/
 13  import data.seq.wseq
src         └───────────┘
 14  universes u v
 15  
 16  namespace computation
 17  open wseq
 18  variables {α : Type u} {β : Type v}
 19  
 20  def parallel.aux2 : list (computation α) → α ⊕ list (computation α) :=
id                       └──┘  └─────────┘       └──┘  └─────────┘ 
src                      └──┘  └─────────┘         └──┘  └─────────┘
typ                      └──┘  └─────────┘       └──┘  └─────────┘ 
doc                            └─────────┘                └─────────┘
 21  list.foldr (λc o, match o with
id   └────────┘            
src  └────────┘
typ  └────────┘            
 22  | sum.inl a  := sum.inl a
id     └─────┘      └─────┘
src    └─────┘       └─────┘
typ    └─────┘      └─────┘
 23  | sum.inr ls := rmap (λ c', c' :: ls) (destruct c)
id     └─────┘ └┘    └──┘    └┘  └┘ └┘      └──────┘ 
src    └─────┘       └──┘           └┘      └──────┘
typ    └─────┘ └┘    └──┘    └┘  └┘ └┘      └──────┘ 
doc                  └──┘                   └──────┘
 24  end) (sum.inr [])
id         └─────┘ └┘
src        └─────┘ └┘
typ        └─────┘ └┘
 25  
 26  def parallel.aux1 : list (computation α) × wseq (computation α) →
id                       └──┘  └─────────┘    └──┘  └─────────┘   
src                      └──┘  └─────────┘     └──┘  └─────────┘
typ                      └──┘  └─────────┘    └──┘  └─────────┘   
doc                            └─────────┘      └──┘  └─────────┘
 27    α ⊕ list (computation α) × wseq (computation α)
id       └──┘  └─────────┘    └──┘  └─────────┘ 
src       └──┘  └─────────┘     └──┘  └─────────┘
typ      └──┘  └─────────┘    └──┘  └─────────┘ 
doc              └─────────┘      └──┘  └─────────┘
 28  | (l, S) := rmap (λ l', match seq.destruct S with
id            └──┘    └┘        └──────────┘
src             └──┘              └──────────┘
typ           └──┘    └┘        └──────────┘
doc              └──┘              └──────────┘
 29    | none := (l', nil)
id       └──┘    └┘  └─┘
src      └──┘        └─┘
typ      └──┘    └┘  └─┘
doc                   └─┘
 30    | some (none, S') := (l', S')
id       └──┘ └──┘  └┘     └┘
src      └──┘ └──┘         
typ      └──┘ └──┘  └┘     └┘
 31    | some (some c, S') := (c::l', S')
id            └──┘   └┘      └┘└┘
src           └──┘            └┘
typ           └──┘   └┘      └┘└┘
 32    end) (parallel.aux2 l)
id           └───────────┘
src          └───────────┘
typ          └───────────┘
 33  
 34  /-- Parallel computation of an infinite stream of computations,
 35    taking the first result -/
 36  def parallel (S : wseq (computation α)) : computation α :=
id                     └──┘  └─────────┘      └─────────┘ 
src                    └──┘  └─────────┘       └─────────┘
typ                    └──┘  └─────────┘      └─────────┘ 
doc                    └──┘  └─────────┘       └─────────┘
 37  corec parallel.aux1 ([], S)
id   └───┘ └───────────┘ └┘  
src  └───┘ └───────────┘ └┘
typ  └───┘ └───────────┘ └┘  
doc  └───┘
 38  
 39  theorem terminates_parallel.aux : ∀ {l : list (computation α)} {S c},
id                                            └──┘  └─────────┘      
src                                           └──┘  └─────────┘
typ                                           └──┘  └─────────┘      
doc                                                 └─────────┘
 40    c ∈ l → terminates c → terminates (corec parallel.aux1 (l, S)) :=
id          └────────┘    └────────┘  └───┘ └───────────┘   
src           └────────┘     └────────┘  └───┘ └───────────┘ 
typ         └────────┘    └────────┘  └───┘ └───────────┘   
doc            └────────┘     └────────┘  └───┘
 41  begin
st   └─────
 42    have lem1 : ∀ l S, (∃ (a : α), parallel.aux2 l = sum.inl a) →
id                                 └───────────┘    └─────┘
src    └──────────┘ └──┘  └────┘ └───────────┘ └─────┘ └┘ 
typ    └──────────┘ └──┘  └────┘└───────────┘ └─────┘ └┘ 
doc    └──────────┘ └──┘   └────┘                         └┘ 
txt    └──────────┘ └──┘   └────┘                         └┘ 
par    └──────────┘ └──┘   └────┘                         └┘ 
pid    └───────┘└─┘ └──┘   └────┘                         └┘ 
st   ────────────────────────────────────────────────────────────────
 43      terminates (corec parallel.aux1 (l, S)),
id       └────────┘  └───┘ └───────────┘ 
src  ───┘└────────┘ └───┘└───────────┘ └┘ └┘
typ  ───┘└────────┘ └───┘└───────────┘ └┘ └┘
doc  ───┘└────────┘ └───┘               └┘ └┘
txt  ───┘                               └┘ └┘
par  ───┘                               └┘ └┘
pid  ───┘                               └┘ └┘
st   ──────────────────────────────────────────┘└─
 44    { intros l S e, cases e with a e,
id                           
src      └──────────┘  └────┘ └───────┘
typ      └──────────┘  └────┘└───────┘
doc      └──────────┘  └────┘ └───────┘
txt      └──────────┘  └────┘ └───────┘
par      └──────────┘  └────┘ └───────┘
pid            └────┘        └───────┘
st   ───┘└──────────┘└────────────────┘└─
 45      have this : corec parallel.aux1 (l, S) = return a,
id                   └───┘ └───────────┘       └────┘ 
src      └──────────┘└───┘└───────────┘ └┘ └┘ └────┘
typ      └──────────┘└───┘└───────────┘└┘└┘ └────┘
doc      └──────────┘└───┘               └┘ └┘ └────┘
txt      └──────────┘                    └┘ └┘       
par      └──────────┘                    └┘ └┘       
pid      └───────┘└─┘                    └┘ └┘       
st   ────────────────────────────────────────────────────┘└─
 46      { apply destruct_eq_ret, simp [parallel.aux1], rw e, simp [rmap] },
id               └─────────────┘        └───────────┘              └──┘
src        └────┘└─────────────┘  └────┘└───────────┘  └─┘   └────┘└──┘└┘
typ        └────┘└─────────────┘  └────┘└───────────┘  └─┘  └────┘└──┘└┘
doc        └────┘                 └────┘               └─┘   └────┘└──┘└┘
txt        └────┘                 └────┘               └─┘   └────┘    └┘
par        └────┘                 └────┘               └─┘   └────┘    └┘
pid                                                              
st   ─────┘└───────────────────┘└────────────────────┘└────┘└────────────┘└┘
 47      rw this, apply_instance },
id          └──┘
src      └─┘      └─────────────┘
typ      └─┘└──┘  └─────────────┘
doc      └─┘      └─────────────┘
txt      └─┘      └─────────────┘
par      └─┘      └─────────────┘
pid                            
st   ──────────┘└───────────────┘└┘
 48    intros l S c m T, revert l S,
src    └──────────────┘  └────────┘
typ    └──────────────┘  └────────┘
doc    └──────────────┘  └────────┘
txt    └──────────────┘  └────────┘
par    └──────────────┘  └────────┘
pid          └────────┘        └──┘
st   ─────────────────┘└──────────┘└─
 49    apply @terminates_rec_on _ _ c T _ _,
id            └───────────────┘      
src    └────┘ └───────────────┘└───┘  └──┘
typ    └────┘ └───────────────┘└───┘└──┘
doc    └────┘                  └───┘  └──┘
txt    └────┘                  └───┘  └──┘
par    └────┘                  └───┘  └──┘
pid                           └───┘  └──┘
st   ─────────────────────────────────────┘└─
 50    { intros a l S m, apply lem1,
src      └────────────┘  └────┘
typ      └────────────┘  └────┘
doc      └────────────┘  └────┘
txt      └────────────┘  └────┘
par      └────────────┘  └────┘
pid            └──────┘       
st   ───┘└────────────┘└──────────┘└─
 51      induction l with c l IH generalizing m; simp at m, { contradiction },
id                 
src      └────────┘ └─────────────────────────┘  └───────┘    └────────────┘
typ      └────────┘└─────────────────────────┘  └───────┘    └────────────┘
doc      └────────┘ └─────────────────────────┘  └───────┘    └────────────┘
txt      └────────┘ └─────────────────────────┘  └───────┘    └────────────┘
par      └────────┘ └─────────────────────────┘  └───────┘    └────────────┘
pid                └─────────┘└─────────────┘      └──┘                 
st   ────────────────────────────────────────────────────┘└──┘└────────────┘└┘
 52      cases m with e m,
id             
src      └────┘ └───────┘
typ      └────┘└───────┘
doc      └────┘ └───────┘
txt      └────┘ └───────┘
par      └────┘ └───────┘
pid            └───────┘
st   ───────────────────┘└─
 53      { rw ←e, simp [parallel.aux2],
id                     └───────────┘
src        └──┘   └────┘└───────────┘
typ        └──┘  └────┘└───────────┘
doc        └──┘   └────┘             
txt        └──┘   └────┘             
par        └──┘   └────┘             
pid          └┘                    
st   ─────┘└───┘└────────────────────┘└─
 54        cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a' ls,
id               └────────┘ └────────────────────┘  └─────┘ └──────┘  
src        └────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘ └─────────┘
typ        └────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘└─────────┘
doc        └────┘                                                └┘ └─────────┘
txt        └────┘                                                └┘ └─────────┘
par        └────┘                                                └┘ └─────────┘
pid                                                             └┘ └─────────┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
 55        exacts [⟨a', rfl⟩, ⟨a, rfl⟩] },
id                  └┘  └─┘      └─┘
src        └──────┘   └┘└─┘└─┘  └┘└─┘└─┘
typ        └──────┘ └┘└┘└─┘└─┘ └┘└─┘└─┘
doc        └──────┘   └┘   └─┘  └┘   └─┘
txt        └──────┘   └┘   └─┘  └┘   └─┘
par        └──────┘   └┘   └─┘  └┘   └─┘
pid              └┘   └┘   └─┘  └┘   └┘
st   ──────────────────────────────────┘└┘
 56      { cases IH m with a' e,
id               └┘ 
src        └────┘   └────────┘
typ        └────┘└┘└────────┘
doc        └────┘   └────────┘
txt        └────┘   └────────┘
par        └────┘   └────────┘
pid                └────────┘
st   ─────────────────────────┘└─
 57        simp [parallel.aux2], simp [parallel.aux2] at e,
id               └───────────┘         └───────────┘
src        └────┘└───────────┘  └────┘└───────────┘└────┘
typ        └────┘└───────────┘  └────┘└───────────┘└────┘
doc        └────┘               └────┘             └────┘
txt        └────┘               └────┘             └────┘
par        └────┘               └────┘             └────┘
pid                                            └──┘
st   ─────────────────────────┘└─────────────────────────┘└─
 58        rw e, exact ⟨a', rfl⟩ } },
id                     └┘  └─┘
src        └─┘   └────┘   └┘└─┘└┘
typ        └─┘  └────┘ └┘└┘└─┘└┘
doc        └─┘   └────┘   └┘   └┘
txt        └─┘   └────┘   └┘   └┘
par        └─┘   └────┘   └┘   └┘
pid                     └┘   
st   ─────────┘└────────────────┘└──┘
 59    { intros s IH l S m,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid            └─────────┘
st   ────────────────────┘└─
 60      have H1 : ∀ l', parallel.aux2 l = sum.inr l' → s ∈ l',
id                       └───────────┘   └─────┘       
src      └────────┘ └─┘ └───────────┘  └─────┘    
typ      └────────┘ └─┘ └───────────┘└─────┘   
doc      └────────┘ └─┘                            
txt      └────────┘ └─┘                            
par      └────────┘ └─┘                            
pid      └─────┘└─┘ └─┘                            
st   ────────────────────────────────────────────────────────┘└─
 61      { induction l with c l IH' generalizing m;
id                   
src        └────────┘ └──────────────────────────┘
typ        └────────┘└──────────────────────────┘
doc        └────────┘ └──────────────────────────┘
txt        └────────┘ └──────────────────────────┘
par        └────────┘ └──────────────────────────┘
pid                  └──────────┘└─────────────┘
st   ─────┘└────────────────────────────────────────
 62        intros l' e'; simp at m, { contradiction },
src        └──────────┘  └───────┘    └────────────┘
typ        └──────────┘  └───────┘    └────────────┘
doc        └──────────┘  └───────┘    └────────────┘
txt        └──────────┘  └───────┘    └────────────┘
par        └──────────┘  └───────┘    └────────────┘
pid              └────┘      └──┘                 
st   ────────────────────────────┘└──┘└────────────┘└┘
 63        cases m with e m; simp [parallel.aux2] at e',
id                                └───────────┘
src        └────┘ └───────┘  └────┘└───────────┘└─────┘
typ        └────┘└───────┘  └────┘└───────────┘└─────┘
doc        └────┘ └───────┘  └────┘             └─────┘
txt        └────┘ └───────┘  └────┘             └─────┘
par        └────┘ └───────┘  └────┘             └─────┘
pid              └───────┘                   └───┘
st   ─────────────────────────────────────────────────┘└─
 64        { rw ←e at e',
id               
src          └──┘ └────┘
typ          └──┘└────┘
doc          └──┘ └────┘
txt          └──┘ └────┘
par          └──┘ └────┘
pid            └┘ └────┘
st   ───────┘└─────────┘└─
 65          cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a' ls;
id                 └────────┘ └────────────────────┘  └─────┘ └──────┘  
src          └────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘ └─────────┘
typ          └────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘└─────────┘
doc          └────┘                                                └┘ └─────────┘
txt          └────┘                                                └┘ └─────────┘
par          └────┘                                                └┘ └─────────┘
pid                                                               └┘ └─────────┘
st   ─────────────────────────────────────────────────────────────────────────────────
 66          injection e' with e', rw ←e', simp },
id                     └┘              └┘
src          └────────┘  └──────┘  └──┘    └───┘
typ          └────────┘└┘└──────┘  └──┘└┘  └───┘
doc          └────────┘  └──────┘  └──┘    └───┘
txt          └────────┘  └──────┘  └──┘    └───┘
par          └────────┘  └──────┘  └──┘    └───┘
pid                     └──────┘    └┘        
st   ───────────────────────────┘└──────┘└─────┘└┘
 67        { induction e : list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a' ls;
id                         └────────┘ └────────────────────┘  └─────┘ └──────┘  
src          └────────┘ └─┘└────────┘└────────────────────┘ └─────┘└──────┘└┘ └─────────┘
typ          └────────┘ └─┘└────────┘└────────────────────┘ └─────┘└──────┘└┘└─────────┘
doc          └────────┘ └─┘                                                └┘ └─────────┘
txt          └────────┘ └─┘                                                └┘ └─────────┘
par          └────────┘ └─┘                                                └┘ └─────────┘
pid                    └─┘                                                └┘ └────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────
 68          rw e at e', { contradiction },
id              
src          └─┘ └────┘    └────────────┘
typ          └─┘└────┘    └────────────┘
doc          └─┘ └────┘    └────────────┘
txt          └─┘ └────┘    └────────────┘
par          └─┘ └────┘    └────────────┘
pid             └────┘                 
st   ──────────┘└────┘└──┘└────────────┘└┘
 69          have := IH' m _ e,
id                   └─┘    
src          └──────┘    └─┘
typ          └──────┘└─┘└─┘
doc          └──────┘    └─┘
txt          └──────┘    └─┘
par          └──────┘    └─┘
pid          └───┘└─┘    └─┘
st   ────────────────────────┘└─
 70          simp [parallel.aux2] at e',
id                 └───────────┘
src          └────┘└───────────┘└─────┘
typ          └────┘└───────────┘└─────┘
doc          └────┘             └─────┘
txt          └────┘             └─────┘
par          └────┘             └─────┘
pid                           └───┘
st   ─────────────────────────────────┘└─
 71          cases destruct c; injection e' with h',
id                 └──────┘             └┘
src          └────┘└──────┘   └────────┘  └──────┘
typ          └────┘└──────┘  └────────┘└┘└──────┘
doc          └────┘└──────┘   └────────┘  └──────┘
txt          └────┘           └────────┘  └──────┘
par          └────┘           └────────┘  └──────┘
pid                                     └──────┘
st   ─────────────────────────────────────────────┘└─
 72          rw ←h', simp [this] } },
id               └┘        └──┘
src          └──┘    └────┘    └┘
typ          └──┘└┘  └────┘└──┘└┘
doc          └──┘    └────┘    └┘
txt          └──┘    └────┘    └┘
par          └──┘    └────┘    └┘
pid            └┘            
st   ─────────────┘└────────────┘└──┘
 73      induction h : parallel.aux2 l with a l',
id                     └───────────┘ 
src      └────────┘ └─┘└───────────┘ └────────┘
typ      └────────┘ └─┘└───────────┘└────────┘
doc      └────────┘ └─┘              └────────┘
txt      └────────┘ └─┘              └────────┘
par      └────────┘ └─┘              └────────┘
pid                └─┘              └───────┘
st   ──────────────────────────────────────────┘└─
 74      { exact lem1 _ _ ⟨a, h⟩ },
id               └──┘        
src        └────┘    └───┘  └┘ └┘
typ        └────┘└──┘└───┘ └┘└┘
doc        └────┘    └───┘  └┘ └┘
txt        └────┘    └───┘  └┘ └┘
par        └────┘    └───┘  └┘ └┘
pid                 └───┘  └┘ 
st   ─────┘└────────────────────┘└┘
 75      { have H2 : corec parallel.aux1 (l, S) = think _,
id                   └───┘ └───────────┘       └───┘
src        └────────┘└───┘└───────────┘ └┘ └┘ └───┘└┘
typ        └────────┘└───┘└───────────┘└┘└┘ └───┘└┘
doc        └────────┘└───┘               └┘ └┘ └───┘└┘
txt        └────────┘                    └┘ └┘      └┘
par        └────────┘                    └┘ └┘      └┘
pid        └─────┘└─┘                    └┘ └┘      └┘
st   ───────────────────────────────────────────────────┘└─
 76        { apply destruct_eq_think,
id                 └───────────────┘
src          └────┘└───────────────┘
typ          └────┘└───────────────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────┘└─────────────────────┘└─
 77          simp [parallel.aux1],
id                 └───────────┘
src          └────┘└───────────┘
typ          └────┘└───────────┘
doc          └────┘             
txt          └────┘             
par          └────┘             
pid                           
st   ───────────────────────────┘└─
 78          rw h, simp [rmap] },
id                      └──┘
src          └─┘   └────┘└──┘└┘
typ          └─┘  └────┘└──┘└┘
doc          └─┘   └────┘└──┘└┘
txt          └─┘   └────┘    └┘
par          └─┘   └────┘    └┘
pid                       
st   ───────────┘└────────────┘└┘
 79        rw H2, apply @computation.think_terminates _ _ _,
id            └┘         └──────────────────────────┘
src        └─┘    └────┘ └──────────────────────────┘└────┘
typ        └─┘└┘  └────┘ └──────────────────────────┘└────┘
doc        └─┘    └────┘                             └────┘
txt        └─┘    └────┘                             └────┘
par        └─┘    └────┘                             └────┘
pid                                                └────┘
st   ──────────┘└─────────────────────────────────────────┘└─
 80        have := H1 _ h,
id                 └┘   
src        └──────┘  └─┘
typ        └──────┘└┘└─┘
doc        └──────┘  └─┘
txt        └──────┘  └─┘
par        └──────┘  └─┘
pid        └───┘└─┘  └─┘
st   ───────────────────┘└─
 81        rcases seq.destruct S with _ | ⟨_|c, S'⟩;
id                └──────────┘ 
src        └─────┘└──────────┘ └─────────────────┘
typ        └─────┘└──────────┘└─────────────────┘
doc        └─────┘└──────────┘ └─────────────────┘
txt        └─────┘             └─────────────────┘
par        └─────┘             └─────────────────┘
pid                           └─────────────────┘
st   ────────────────────────────────────────────────
 82        simp [parallel.aux1]; apply IH; simp [this] } }
id               └───────────┘                   └──┘
src        └────┘└───────────┘  └────┘    └────┘    └┘
typ        └────┘└───────────┘  └────┘    └────┘└──┘└┘
doc        └────┘               └────┘    └────┘    └┘
txt        └────┘               └────┘    └────┘    └┘
par        └────┘               └────┘    └────┘    └┘
pid                                            
st   ─────────────────────────────────────────────────┘└───
 83  end
st   ──┘
 84  
 85  theorem terminates_parallel {S : wseq (computation α)}
id                                    └──┘  └─────────┘ 
src                                   └──┘  └─────────┘
typ                                   └──┘  └─────────┘ 
doc                                   └──┘  └─────────┘
 86     {c} (h : c ∈ S) [T : terminates c] : terminates (parallel S) :=
id                        └────────┘     └────────┘  └──────┘ 
src                         └────────┘      └────────┘  └──────┘
typ                       └────────┘     └────────┘  └──────┘ 
doc                          └────────┘      └────────┘  └──────┘
 87  suffices ∀ n (l : list (computation α)) S c,
id                    └──┘  └─────────┘     
src                    └──┘  └─────────┘
typ                   └──┘  └─────────┘     
doc                          └─────────┘
 88    c ∈ l ∨ some (some c) = seq.nth S n →
id         └──┘  └──┘    └─────┘  
src          └──┘  └──┘     └─────┘
typ        └──┘  └──┘    └─────┘  
doc                            └─────┘
 89    terminates c → terminates (corec parallel.aux1 (l, S)),
id     └────────┘    └────────┘  └───┘ └───────────┘   
src    └────────┘     └────────┘  └───┘ └───────────┘ 
typ    └────────┘    └────────┘  └───┘ └───────────┘   
doc    └────────┘     └────────┘  └───┘
 90  from let ⟨n, h⟩ := h in this n [] S c (or.inr h) T,
id        └─┘             └──┘   └┘    └────┘    
src                                 └┘      └────┘
typ       └─┘             └──┘   └┘    └────┘    
 91  begin
st   └─────
 92    intro n, induction n with n IH; intros l S c o T,
id                        
src    └─────┘  └────────┘ └────────┘  └──────────────┘
typ    └─────┘  └────────┘└────────┘  └──────────────┘
doc    └─────┘  └────────┘ └────────┘  └──────────────┘
txt    └─────┘  └────────┘ └────────┘  └──────────────┘
par    └─────┘  └────────┘ └────────┘  └──────────────┘
pid         └┘            └───────┘        └────────┘
st   ────────┘└───────────────────────────────────────┘└─
 93    { cases o with a a, { exact terminates_parallel.aux a T },
id                                └─────────────────────┘  
src      └────┘ └───────┘    └────┘└─────────────────────┘  
typ      └────┘└───────┘    └────┘└─────────────────────┘
doc      └────┘ └───────┘    └────┘                         
txt      └────┘ └───────┘    └────┘                         
par      └────┘ └───────┘    └────┘                         
pid            └───────┘                                  
st   ───┘└──────────────┘└──┘└────────────────────────────────┘└┘
 94      have H : seq.destruct S = some (some c, _),
id                └──────────┘        └──┘ 
src      └───────┘└──────────┘     └──┘ └──┘
typ      └───────┘└──────────┘    └──┘└──┘
doc      └───────┘└──────────┘            └──┘
txt      └───────┘                        └──┘
par      └───────┘                        └──┘
pid      └────┘└─┘                        └──┘
st   ─────────────────────────────────────────────┘└─
 95      { unfold seq.destruct functor.map, rw ← a, simp },
id                                               
src        └─────────────────────────────┘  └───┘   └───┘
typ        └─────────────────────────────┘  └───┘  └───┘
doc        └─────────────────────────────┘  └───┘   └───┘
txt        └─────────────────────────────┘  └───┘   └───┘
par        └─────────────────────────────┘  └───┘   └───┘
pid              └───────────────────────┘    └─┘       
st   ─────┘└─────────────────────────────┘└──────┘└─────┘└┘
 96      induction h : parallel.aux2 l with a l';
id                     └───────────┘ 
src      └────────┘ └─┘└───────────┘ └────────┘
typ      └────────┘ └─┘└───────────┘└────────┘
doc      └────────┘ └─┘              └────────┘
txt      └────────┘ └─┘              └────────┘
par      └────────┘ └─┘              └────────┘
pid                └─┘              └───────┘
st   ─────────────────────────────────────────────
 97      have C : corec parallel.aux1 (l, S) = _,
id                └───┘ └───────────┘   
src      └───────┘└───┘└───────────┘ └┘ └┘ └┘
typ      └───────┘└───┘└───────────┘└┘└┘ └┘
doc      └───────┘└───┘               └┘ └┘ └┘
txt      └───────┘                    └┘ └┘ └┘
par      └───────┘                    └┘ └┘ └┘
pid      └────┘└─┘                    └┘ └┘ └┘
st   ──────────────────────────────────────────┘└─
 98      { apply destruct_eq_ret, simp [parallel.aux1], rw [h], simp [rmap] },
id               └─────────────┘        └───────────┘                └──┘
src        └────┘└─────────────┘  └────┘└───────────┘  └──┘   └────┘└──┘└┘
typ        └────┘└─────────────┘  └────┘└───────────┘  └──┘  └────┘└──┘└┘
doc        └────┘                 └────┘               └──┘   └────┘└──┘└┘
txt        └────┘                 └────┘               └──┘   └────┘    └┘
par        └────┘                 └────┘               └──┘   └────┘    └┘
pid                                                   └┘           
st   ─────┘└───────────────────┘└────────────────────┘└─────┘└─────────────┘└┘
 99      { rw C, resetI, apply_instance },
id            
src        └─┘   └────┘  └─────────────┘
typ        └─┘  └────┘  └─────────────┘
doc        └─┘   └────┘  └─────────────┘
txt        └─┘   └────┘  └─────────────┘
par        └─┘   └────┘  └─────────────┘
pid                                   
st   ─────┘└──┘└───────────────────────┘└┘
100      { apply destruct_eq_think, simp [parallel.aux1], rw [h, H], simp [rmap] },
id               └───────────────┘        └───────────┘                  └──┘
src        └────┘└───────────────┘  └────┘└───────────┘  └──┘ └┘   └────┘└──┘└┘
typ        └────┘└───────────────┘  └────┘└───────────┘  └──┘└┘  └────┘└──┘└┘
doc        └────┘                   └────┘               └──┘ └┘   └────┘└──┘└┘
txt        └────┘                   └────┘               └──┘ └┘   └────┘    └┘
par        └────┘                   └────┘               └──┘ └┘   └────┘    └┘
pid                                                     └┘ └┘           
st   ─────┘└─────────────────────┘└────────────────────┘└─────┘└─┘└─────────────┘└┘
101      { rw C, apply @computation.think_terminates _ _ _,
id                     └──────────────────────────┘
src        └─┘   └────┘ └──────────────────────────┘└────┘
typ        └─┘  └────┘ └──────────────────────────┘└────┘
doc        └─┘   └────┘                             └────┘
txt        └─┘   └────┘                             └────┘
par        └─┘   └────┘                             └────┘
pid                                               └────┘
st   ─────────┘└─────────────────────────────────────────┘└─
102        apply terminates_parallel.aux _ T, simp } },
id               └─────────────────────┘   
src        └────┘└─────────────────────┘└─┘   └───┘
typ        └────┘└─────────────────────┘└─┘  └───┘
doc        └────┘                       └─┘   └───┘
txt        └────┘                       └─┘   └───┘
par        └────┘                       └─┘   └───┘
pid                                    └─┘       
st   ──────────────────────────────────────┘└─────┘└──┘
103    { cases o with a a, { exact terminates_parallel.aux a T },
id                                └─────────────────────┘  
src      └────┘ └───────┘    └────┘└─────────────────────┘  
typ      └────┘└───────┘    └────┘└─────────────────────┘
doc      └────┘ └───────┘    └────┘                         
txt      └────┘ └───────┘    └────┘                         
par      └────┘ └───────┘    └────┘                         
pid            └───────┘                                  
st   ───────────────────┘└──┘└────────────────────────────────┘└┘
104      induction h : parallel.aux2 l with a l';
id                     └───────────┘ 
src      └────────┘ └─┘└───────────┘ └────────┘
typ      └────────┘ └─┘└───────────┘└────────┘
doc      └────────┘ └─┘              └────────┘
txt      └────────┘ └─┘              └────────┘
par      └────────┘ └─┘              └────────┘
pid                └─┘              └───────┘
st   ─────────────────────────────────────────────
105      have C : corec parallel.aux1 (l, S) = _,
id                └───┘ └───────────┘   
src      └───────┘└───┘└───────────┘ └┘ └┘ └┘
typ      └───────┘└───┘└───────────┘└┘└┘ └┘
doc      └───────┘└───┘               └┘ └┘ └┘
txt      └───────┘                    └┘ └┘ └┘
par      └───────┘                    └┘ └┘ └┘
pid      └────┘└─┘                    └┘ └┘ └┘
st   ──────────────────────────────────────────┘└─
106      { apply destruct_eq_ret, simp [parallel.aux1], rw [h], simp [rmap] },
id               └─────────────┘        └───────────┘                └──┘
src        └────┘└─────────────┘  └────┘└───────────┘  └──┘   └────┘└──┘└┘
typ        └────┘└─────────────┘  └────┘└───────────┘  └──┘  └────┘└──┘└┘
doc        └────┘                 └────┘               └──┘   └────┘└──┘└┘
txt        └────┘                 └────┘               └──┘   └────┘    └┘
par        └────┘                 └────┘               └──┘   └────┘    └┘
pid                                                   └┘           
st   ─────┘└───────────────────┘└────────────────────┘└─────┘└─────────────┘└┘
107      { rw C, resetI, apply_instance },
id            
src        └─┘   └────┘  └─────────────┘
typ        └─┘  └────┘  └─────────────┘
doc        └─┘   └────┘  └─────────────┘
txt        └─┘   └────┘  └─────────────┘
par        └─┘   └────┘  └─────────────┘
pid                                   
st   ─────┘└──┘└───────────────────────┘└┘
108      { apply destruct_eq_think, simp [parallel.aux1], rw [h], simp [rmap] },
id               └───────────────┘        └───────────┘                └──┘
src        └────┘└───────────────┘  └────┘└───────────┘  └──┘   └────┘└──┘└┘
typ        └────┘└───────────────┘  └────┘└───────────┘  └──┘  └────┘└──┘└┘
doc        └────┘                   └────┘               └──┘   └────┘└──┘└┘
txt        └────┘                   └────┘               └──┘   └────┘    └┘
par        └────┘                   └────┘               └──┘   └────┘    └┘
pid                                                     └┘           
st   ─────┘└─────────────────────┘└────────────────────┘└─────┘└─────────────┘└┘
109      { rw C, apply @computation.think_terminates _ _ _,
id                     └──────────────────────────┘
src        └─┘   └────┘ └──────────────────────────┘└────┘
typ        └─┘  └────┘ └──────────────────────────┘└────┘
doc        └─┘   └────┘                             └────┘
txt        └─┘   └────┘                             └────┘
par        └─┘   └────┘                             └────┘
pid                                               └────┘
st   ─────────┘└─────────────────────────────────────────┘└─
110        have TT : ∀ l', terminates (corec parallel.aux1 (l', S.tail)),
id                         └────────┘  └───┘ └───────────┘     └────┘
src        └────────┘ └─┘ └────────┘ └───┘└───────────┘  └┘└────┘└┘
typ        └────────┘ └─┘ └────────┘ └───┘└───────────┘  └┘└────┘└┘
doc        └────────┘ └─┘ └────────┘ └───┘                └┘└────┘└┘
txt        └────────┘ └─┘                                 └┘      └┘
par        └────────┘ └─┘                                 └┘      └┘
pid        └─────┘└─┘ └─┘                                 └┘      └┘
st   ──────────────────────────────────────────────────────────────────┘└─
111        { intro, apply IH _ _ _ (or.inr _) T, rw a, cases S with f al, refl },
id                        └┘        └────┘                 
src          └───┘  └────┘  └─────┘ └────┘└──┘   └─┘   └────┘ └────────┘  └───┘
typ          └───┘  └────┘└┘└─────┘ └────┘└──┘  └─┘  └────┘└────────┘  └───┘
doc          └───┘  └────┘  └─────┘       └──┘   └─┘   └────┘ └────────┘  └───┘
txt          └───┘  └────┘  └─────┘       └──┘   └─┘   └────┘ └────────┘  └───┘
par          └───┘  └────┘  └─────┘       └──┘   └─┘   └────┘ └────────┘  └───┘
pid                        └─────┘       └──┘              └────────┘      
st   ───────┘└───┘└───────────────────────────┘└────┘└─────────────────┘└─────┘└┘
112        induction e : seq.nth S 0 with o,
id                       └─────┘ 
src        └────────┘ └─┘└─────┘ └───────┘
typ        └────────┘ └─┘└─────┘└───────┘
doc        └────────┘ └─┘└─────┘ └───────┘
txt        └────────┘ └─┘        └───────┘
par        └────────┘ └─┘        └───────┘
pid                  └─┘        └┘└────┘
st   ─────────────────────────────────────┘└─
113        { have D : seq.destruct S = none,
id                    └──────────┘    └──┘
src          └───────┘└──────────┘  └──┘
typ          └───────┘└──────────┘ └──┘
doc          └───────┘└──────────┘  
txt          └───────┘              
par          └───────┘              
pid          └────┘└─┘              
st   ───────┘└────────────────────────────┘└─
114          { dsimp [seq.destruct], rw e, refl },
id                    └──────────┘      
src            └─────┘└──────────┘  └─┘   └───┘
typ            └─────┘└──────────┘  └─┘  └───┘
doc            └─────┘└──────────┘  └─┘   └───┘
txt            └─────┘              └─┘   └───┘
par            └─────┘              └─┘   └───┘
pid                                        
st   ─────────┘└──────────────────┘└────┘└─────┘└┘
115          rw D, simp [parallel.aux1], have TT := TT l',
id                      └───────────┘              └┘ └┘
src          └─┘   └────┘└───────────┘  └─────────┘  
typ          └─┘  └────┘└───────────┘  └─────────┘└┘└┘
doc          └─┘   └────┘               └─────────┘  
txt          └─┘   └────┘               └─────────┘  
par          └─┘   └────┘               └─────────┘  
pid                                  └─────┘└─┘  
st   ───────────┘└────────────────────┘└────────────────┘└─
116          rwa [seq.destruct_eq_nil D, seq.tail_nil] at TT },
id                └─────────────────┘   └──────────┘
src          └───┘└─────────────────┘ └┘└──────────┘└──────┘
typ          └───┘└─────────────────┘└┘└──────────┘└──────┘
doc          └───┘                    └┘            └──────┘
txt          └───┘                    └┘            └──────┘
par          └───┘                    └┘            └──────┘
pid             └┘                    └┘            └────┘
st   ─────────────────────────────────┘└────────────┘└─────┘└┘
117        { have D : seq.destruct S = some (o, S.tail),
id                    └──────────┘     └──┘   └────┘
src          └───────┘└──────────┘  └──┘ └┘└────┘
typ          └───────┘└──────────┘  └──┘└┘└────┘
doc          └───────┘└──────────┘        └┘└────┘
txt          └───────┘                    └┘      
par          └───────┘                    └┘      
pid          └────┘└─┘                    └┘      
st   ─────────────────────────────────────────────────┘└─
118          { dsimp [seq.destruct], rw e, refl },
id                    └──────────┘      
src            └─────┘└──────────┘  └─┘   └───┘
typ            └─────┘└──────────┘  └─┘  └───┘
doc            └─────┘└──────────┘  └─┘   └───┘
txt            └─────┘              └─┘   └───┘
par            └─────┘              └─┘   └───┘
pid                                        
st   ─────────┘└──────────────────┘└────┘└─────┘└┘
119          rw D, cases o with c; simp [parallel.aux1, TT] } } }
id                                     └───────────┘  └┘
src          └─┘   └────┘ └─────┘  └────┘└───────────┘└┘  └┘
typ          └─┘  └────┘└─────┘  └────┘└───────────┘└┘└┘└┘
doc          └─┘   └────┘ └─────┘  └────┘             └┘  └┘
txt          └─┘   └────┘ └─────┘  └────┘             └┘  └┘
par          └─┘   └────┘ └─────┘  └────┘             └┘  └┘
pid                     └─────┘                   └┘  
st   ───────────┘└─────────────────────────────────────────┘└─────
120  end
st   ──┘
121  
122  theorem exists_of_mem_parallel {S : wseq (computation α)}
id                                       └──┘  └─────────┘ 
src                                      └──┘  └─────────┘
typ                                      └──┘  └─────────┘ 
doc                                      └──┘  └─────────┘
123     {a} (h : a ∈ parallel S) : ∃ c ∈ S, a ∈ c :=
id                 └──────┘            
src                 └──────┘               
typ                └──────┘            
doc                  └──────┘
124  suffices ∀ C, a ∈ C → ∀ (l : list (computation α)) S,
id                            └──┘  └─────────┘    
src                              └──┘  └─────────┘
typ                           └──┘  └─────────┘    
doc                                     └─────────┘
125    corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c,
id     └───┘ └───────────┘                       
src    └───┘ └───────────┘                               
typ    └───┘ └───────────┘                       
doc    └───┘
126  from let ⟨c, h1, h2⟩ := this _ h [] S rfl in ⟨c, h1.resolve_left id, h2⟩,
id        └─┘    └┘  └┘     └──┘    └┘  └─┘          └───────────┘ └┘
src                                   └┘   └─┘          └───────────┘ └┘
typ       └─┘    └┘  └┘     └──┘    └┘  └─┘          └───────────┘ └┘
127  begin
st   └─────
128    let F : list (computation α) → α ⊕ list (computation α) → Prop,
id             └──┘                      └──┘  └─────────┘ 
src    └──────┘                 └┘  └──┘ └─────────┘ └┘ 
typ    └──────┘└──┘             └┘  └──┘ └─────────┘└┘ 
doc    └──────┘                 └┘        └─────────┘ └┘ 
txt    └──────┘                 └┘                    └┘ 
par    └──────┘                 └┘                    └┘ 
pid    └───┘└─┘                 └┘                    └┘ 
st   ───────────────────────────────────────────────────────────────┘└─
129    { intros l a, cases a with a l',
id                         
src      └────────┘  └────┘ └────────┘
typ      └────────┘  └────┘└────────┘
doc      └────────┘  └────┘ └────────┘
txt      └────────┘  └────┘ └────────┘
par      └────────┘  └────┘ └────────┘
pid            └──┘        └────────┘
st   ───┘└────────┘└─────────────────┘└─
130      exact ∃ c ∈ l, a ∈ c,
id                   
src      └────┘└───┘   
typ      └────┘└───┘ 
doc      └────┘ └───┘    
txt      └────┘ └───┘    
par      └────┘ └───┘    
pid            └───┘    
st   ───────────────────────┘└─
131      exact ∀ a', (∃ c ∈ l', a' ∈ c) → (∃ c ∈ l, a' ∈ c) },
id                         └┘                  
src      └────┘ └─┘   └───┘       └┘   └───┘      └┘
typ      └────┘ └─┘  └───┘└┘    └┘   └───┘     └┘
doc      └────┘ └─┘   └───┘       └┘   └───┘      └┘
txt      └────┘ └─┘   └───┘       └┘   └───┘      └┘
par      └────┘ └─┘   └───┘       └┘   └───┘      └┘
pid            └─┘   └───┘       └┘   └───┘      
st   ──────────────────────────────────────────────────────┘└┘
132    have lem1 : ∀ (l : list (computation α)), F l (parallel.aux2 l),
id                        └──┘  └─────────┘         └───────────┘
src    └──────────┘ └────┘└──┘ └─────────┘ └┘    └───────────┘ 
typ    └──────────┘ └────┘└──┘ └─────────┘└┘   └───────────┘ 
doc    └──────────┘ └────┘     └─────────┘ └┘                  
txt    └──────────┘ └────┘                 └┘                  
par    └──────────┘ └────┘                 └┘                  
pid    └───────┘└─┘ └────┘                 └┘                  
st   ────────────────────────────────────────────────────────────────┘└─
133    { intro l, induction l with c l IH; simp [parallel.aux2],
id                                              └───────────┘
src      └─────┘  └────────┘ └──────────┘  └────┘└───────────┘
typ      └─────┘  └────────┘└──────────┘  └────┘└───────────┘
doc      └─────┘  └────────┘ └──────────┘  └────┘             
txt      └─────┘  └────────┘ └──────────┘  └────┘             
par      └─────┘  └────────┘ └──────────┘  └────┘             
pid           └┘            └─────────┘                   
st   ───┘└─────┘└─────────────────────────────────────────────┘└─
134      { intros a h, rcases h with ⟨c, hn, _⟩,
id                            
src        └────────┘  └─────┘ └──────────────┘
typ        └────────┘  └─────┘└──────────────┘
doc        └────────┘  └─────┘ └──────────────┘
txt        └────────┘  └─────┘ └──────────────┘
par        └────────┘  └─────┘ └──────────────┘
pid              └──┘         └──────────────┘
st   ─────┘└────────┘└────────────────────────┘└─
135        exact false.elim hn },
id               └────────┘ └┘
src        └────┘└────────┘  
typ        └────┘└────────┘└┘
doc        └────┘            
txt        └────┘            
par        └────┘            
pid                         
st   ─────────────────────────┘└┘
136      { simp [parallel.aux2] at IH,
id               └───────────┘
src        └────┘└───────────┘└─────┘
typ        └────┘└───────────┘└─────┘
doc        └────┘             └─────┘
txt        └────┘             └─────┘
par        └────┘             └─────┘
pid                         └───┘
st   ───────────────────────────────┘└─
137        cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a ls;
id               └────────┘ └────────────────────┘  └─────┘ └──────┘  
src        └────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘ └────────┘
typ        └────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘└────────┘
doc        └────┘                                                └┘ └────────┘
txt        └────┘                                                └┘ └────────┘
par        └────┘                                                └┘ └────────┘
pid                                                             └┘ └────────┘
st   ──────────────────────────────────────────────────────────────────────────────
138        simp [parallel.aux2],
id               └───────────┘
src        └────┘└───────────┘
typ        └────┘└───────────┘
doc        └────┘             
txt        └────┘             
par        └────┘             
pid                         
st   ─────────────────────────┘└─
139        { rcases IH with ⟨c', cl, ac⟩,
id                  └┘
src          └─────┘  └────────────────┘
typ          └─────┘└┘└────────────────┘
doc          └─────┘  └────────────────┘
txt          └─────┘  └────────────────┘
par          └─────┘  └────────────────┘
pid                  └────────────────┘
st   ───────┘└─────────────────────────┘└─
140          refine ⟨c', or.inr cl, ac⟩ },
id                   └┘  └────┘ └┘  └┘
src          └─────┘   └┘└────┘  └┘  └┘
typ          └─────┘ └┘└┘└────┘└┘└┘└┘└┘
doc          └─────┘   └┘        └┘  └┘
txt          └─────┘   └┘        └┘  └┘
par          └─────┘   └┘        └┘  └┘
pid                   └┘        └┘  
st   ──────────────────────────────────┘└┘
141        { induction h : destruct c with a c'; simp [rmap],
id                         └──────┘                   └──┘
src          └────────┘ └─┘└──────┘ └────────┘  └────┘└──┘
typ          └────────┘ └─┘└──────┘└────────┘  └────┘└──┘
doc          └────────┘ └─┘└──────┘ └────────┘  └────┘└──┘
txt          └────────┘ └─┘         └────────┘  └────┘    
par          └────────┘ └─┘         └────────┘  └────┘    
pid                    └─┘         └───────┘          
st   ──────────────────────────────────────────────────────┘└─
142          { refine ⟨c, list.mem_cons_self _ _, _⟩,
id                       └────────────────┘
src            └─────┘  └┘└────────────────┘└──────┘
typ            └─────┘ └┘└────────────────┘└──────┘
doc            └─────┘  └┘                  └──────┘
txt            └─────┘  └┘                  └──────┘
par            └─────┘  └┘                  └──────┘
pid                    └┘                  └──────┘
st   ─────────┘└───────────────────────────────────┘└─
143            rw destruct_eq_ret h,
id                └─────────────┘ 
src            └─┘└─────────────┘
typ            └─┘└─────────────┘
doc            └─┘               
txt            └─┘               
par            └─┘               
pid                             
st   ─────────────────────────────┘└─
144            apply ret_mem },
id                   └─────┘
src            └────┘└─────┘
typ            └────┘└─────┘
doc            └────┘       
txt            └────┘       
par            └────┘       
pid                        
st   ───────────────────────┘└┘
145          { intros a' h, rcases h with ⟨d, dm, ad⟩,
id                                 
src            └─────────┘  └─────┘ └───────────────┘
typ            └─────────┘  └─────┘└───────────────┘
doc            └─────────┘  └─────┘ └───────────────┘
txt            └─────────┘  └─────┘ └───────────────┘
par            └─────────┘  └─────┘ └───────────────┘
pid                  └───┘         └───────────────┘
st   ────────────────────┘└─────────────────────────┘└─
146            simp at dm, cases dm with e dl,
id                               └┘
src            └────────┘  └────┘  └────────┘
typ            └────────┘  └────┘└┘└────────┘
doc            └────────┘  └────┘  └────────┘
txt            └────────┘  └────┘  └────────┘
par            └────────┘  └────┘  └────────┘
pid                └───┘         └────────┘
st   ───────────────────┘└──────────────────┘└─
147            { rw e at ad, refine ⟨c, list.mem_cons_self _ _, _⟩,
id                                    └────────────────┘
src              └─┘ └────┘  └─────┘  └┘└────────────────┘└──────┘
typ              └─┘└────┘  └─────┘ └┘└────────────────┘└──────┘
doc              └─┘ └────┘  └─────┘  └┘                  └──────┘
txt              └─┘ └────┘  └─────┘  └┘                  └──────┘
par              └─┘ └────┘  └─────┘  └┘                  └──────┘
pid                 └────┘          └┘                  └──────┘
st   ───────────┘└────────┘└─────────────────────────────────────┘└─
148              rw destruct_eq_think h,
id                  └───────────────┘ 
src              └─┘└───────────────┘
typ              └─┘└───────────────┘
doc              └─┘                 
txt              └─┘                 
par              └─┘                 
pid                                 
st   ─────────────────────────────────┘└─
149              exact think_mem ad },
id                     └───────┘ └┘
src              └────┘└───────┘  
typ              └────┘└───────┘└┘
doc              └────┘           
txt              └────┘           
par              └────┘           
pid                              
st   ──────────────────────────────┘└┘
150            { cases IH a' ⟨d, dl, ad⟩ with d dm, cases dm with dm ad,
id                     └┘ └┘    └┘  └┘                   └┘
src              └────┘      └┘  └┘  └─────────┘  └────┘  └─────────┘
typ              └────┘└┘└┘ └┘└┘└┘└┘└─────────┘  └────┘└┘└─────────┘
doc              └────┘      └┘  └┘  └─────────┘  └────┘  └─────────┘
txt              └────┘      └┘  └┘  └─────────┘  └────┘  └─────────┘
par              └────┘      └┘  └┘  └─────────┘  └────┘  └─────────┘
pid                         └┘  └┘  └────────┘         └─────────┘
st   ────────────────────────────────────────────┘└───────────────────┘└─
151              exact ⟨d, or.inr dm, ad⟩ } } } } },
id                        └────┘ └┘  └┘
src              └────┘  └┘└────┘  └┘  └┘
typ              └────┘ └┘└────┘└┘└┘└┘└┘
doc              └────┘  └┘        └┘  └┘
txt              └────┘  └┘        └┘  └┘
par              └────┘  └┘        └┘  └┘
pid                     └┘        └┘  
st   ────────────────────────────────────┘└────────┘
152    intros C aC, refine mem_rec_on aC _ (λ C' IH, _);
id                         └────────┘ └┘
src    └─────────┘  └─────┘└────────┘  └─┘  └────────┘
typ    └─────────┘  └─────┘└────────┘└┘└─┘  └────────┘
doc    └─────────┘  └─────┘            └─┘  └────────┘
txt    └─────────┘  └─────┘            └─┘  └────────┘
par    └─────────┘  └─────┘            └─┘  └────────┘
pid          └───┘                    └─┘  └────────┘
st   ────────────┘└──────────────────────────────────────
153    intros l S e; have e' := congr_arg destruct e; have := lem1 l;
id                              └───────┘ └──────┘           └──┘ 
src    └──────────┘  └─────────┘└───────┘└──────┘   └──────┘    
typ    └──────────┘  └─────────┘└───────┘└──────┘  └──────┘└──┘
doc    └──────────┘  └─────────┘         └──────┘   └──────┘    
txt    └──────────┘  └─────────┘                    └──────┘    
par    └──────────┘  └─────────┘                    └──────┘    
pid          └────┘  └─────┘└─┘                    └───┘└─┘    
st   ─────────────────────────────────────────────────────────────────
154    simp [parallel.aux1] at e'; cases parallel.aux2 l with a' l'; injection e' with h',
id           └───────────┘               └───────────┘                        └┘
src    └────┘└───────────┘└─────┘  └────┘└───────────┘ └─────────┘  └────────┘  └──────┘
typ    └────┘└───────────┘└─────┘  └────┘└───────────┘└─────────┘  └────────┘└┘└──────┘
doc    └────┘             └─────┘  └────┘              └─────────┘  └────────┘  └──────┘
txt    └────┘             └─────┘  └────┘              └─────────┘  └────────┘  └──────┘
par    └────┘             └─────┘  └────┘              └─────────┘  └────────┘  └──────┘
pid                     └───┘                     └─────────┘             └──────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
155    { rw h' at this, rcases this with ⟨c, cl, ac⟩,
id          └┘                 └──┘
src      └─┘  └──────┘  └─────┘    └───────────────┘
typ      └─┘└┘└──────┘  └─────┘└──┘└───────────────┘
doc      └─┘  └──────┘  └─────┘    └───────────────┘
txt      └─┘  └──────┘  └─────┘    └───────────────┘
par      └─┘  └──────┘  └─────┘    └───────────────┘
pid          └──────┘            └───────────────┘
st   ───┘└───────────┘└────────────────────────────┘└─
156      exact ⟨c, or.inl cl, ac⟩ },
id                └────┘ └┘  └┘
src      └────┘  └┘└────┘  └┘  └┘
typ      └────┘ └┘└────┘└┘└┘└┘└┘
doc      └────┘  └┘        └┘  └┘
txt      └────┘  └┘        └┘  └┘
par      └────┘  └┘        └┘  └┘
pid             └┘        └┘  
st   ────────────────────────────┘└┘
157    { induction e : seq.destruct S with a; rw e at h',
id                     └──────────┘             
src      └────────┘ └─┘└──────────┘ └─────┘  └─┘ └────┘
typ      └────────┘ └─┘└──────────┘└─────┘  └─┘└────┘
doc      └────────┘ └─┘└──────────┘ └─────┘  └─┘ └────┘
txt      └────────┘ └─┘             └─────┘  └─┘ └────┘
par      └────────┘ └─┘             └─────┘  └─┘ └────┘
pid                └─┘             └────┘     └────┘
st   ───────────────────────────────────────────┘└────┘└─
158      { exact let ⟨d, o, ad⟩ := IH _ _ h',
id                        └┘     └┘     └┘
src        └────┘     └┘ └┘  └───┘  └───┘  └─
typ        └────┘    └┘└┘└┘└───┘└┘└───┘└┘└─
doc        └────┘     └┘ └┘  └───┘  └───┘  └─
txt        └────┘     └┘ └┘  └───┘  └───┘  └─
par        └────┘     └┘ └┘  └───┘  └───┘  └─
pid                  └┘ └┘  └───┘  └───┘  └─
st   ─────┘└──────────────────────────────────
159          ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (not_mem_nil _), ad⟩ in
id              └┘  └┘     └──┘       └────────────┘  └─────────┘
src  ───────┘  └┘  └┘  └───┘       └┘ └────────────┘ └─────────┘└───┘  └────
typ  ───────┘ └┘└┘└┘└┘└───┘└──┘  └┘ └────────────┘ └─────────┘└───┘  └────
doc  ───────┘  └┘  └┘  └───┘       └┘                           └───┘  └────
txt  ───────┘  └┘  └┘  └───┘       └┘                           └───┘  └────
par  ───────┘  └┘  └┘  └───┘       └┘                           └───┘  └────
pid  ───────┘  └┘  └┘  └───┘       └┘                           └───┘  └────
st   ──────────────────────────────────────────────────────────────────────────
160        ⟨c, or.inl cl, ac⟩ },
id             └────┘
src  ─────┘  └┘└────┘  └┘  └┘
typ  ─────┘  └┘└────┘  └┘  └┘
doc  ─────┘  └┘        └┘  └┘
txt  ─────┘  └┘        └┘  └┘
par  ─────┘  └┘        └┘  └┘
pid  ─────┘  └┘        └┘  
st   ────────────────────────┘└┘
161      { cases a with o S', cases o with c; simp [parallel.aux1] at h';
id                                                └───────────┘
src        └────┘ └────────┘  └────┘ └─────┘  └────┘└───────────┘└─────┘
typ        └────┘└────────┘  └────┘└─────┘  └────┘└───────────┘└─────┘
doc        └────┘ └────────┘  └────┘ └─────┘  └────┘             └─────┘
txt        └────┘ └────────┘  └────┘ └─────┘  └────┘             └─────┘
par        └────┘ └────────┘  └────┘ └─────┘  └────┘             └─────┘
pid              └────────┘        └─────┘                   └───┘
st   ──────────────────────┘└─────────────────────────────────────────────
162        rcases IH _ _ h' with ⟨d, dl | dS', ad⟩,
id                └┘     └┘
src        └─────┘  └───┘  └─────────────────────┘
typ        └─────┘└┘└───┘└┘└─────────────────────┘
doc        └─────┘  └───┘  └─────────────────────┘
txt        └─────┘  └───┘  └─────────────────────┘
par        └─────┘  └───┘  └─────────────────────┘
pid                └───┘  └─────────────────────┘
st   ────────────────────────────────────────────┘└─
163        { exact let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩ in ⟨c, or.inl cl, ac⟩ },
id                        └┘  └┘     └──┘     └┘  └┘         └────┘
src          └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘└────┘  └┘  └┘
typ          └────┘    └┘└┘└┘└┘└───┘└──┘ └┘└┘└┘└┘└───┘  └┘└────┘  └┘  └┘
doc          └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  └┘
txt          └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  └┘
par          └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  └┘
pid                    └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  
st   ───────┘└────────────────────────────────────────────────────────────────┘└┘
164        { refine ⟨d, or.inr _, ad⟩,
id                     └────┘    └┘
src          └─────┘  └┘└────┘└──┘  
typ          └─────┘ └┘└────┘└──┘└┘
doc          └─────┘  └┘      └──┘  
txt          └─────┘  └┘      └──┘  
par          └─────┘  └┘      └──┘  
pid                  └┘      └──┘  
st   ───────┘└──────────────────────┘└─
165          rw seq.destruct_eq_cons e,
id              └──────────────────┘ 
src          └─┘└──────────────────┘
typ          └─┘└──────────────────┘
doc          └─┘                    
txt          └─┘                    
par          └─┘                    
pid                                
st   ────────────────────────────────┘└─
166          exact seq.mem_cons_of_mem _ dS' },
id                 └─────────────────┘   └─┘
src          └────┘└─────────────────┘└─┘   
typ          └────┘└─────────────────┘└─┘└─┘
doc          └────┘                   └─┘   
txt          └────┘                   └─┘   
par          └────┘                   └─┘   
pid                                  └─┘   
st   ───────────────────────────────────────┘└┘
167        { simp at dl, cases dl with dc dl,
id                             └┘
src          └────────┘  └────┘  └─────────┘
typ          └────────┘  └────┘└┘└─────────┘
doc          └────────┘  └────┘  └─────────┘
txt          └────────┘  └────┘  └─────────┘
par          └────────┘  └────┘  └─────────┘
pid              └───┘         └─────────┘
st   ───────┘└────────┘└───────────────────┘└─
168          { rw dc at ad, refine ⟨c, or.inr _, ad⟩,
id                └┘                  └────┘    └┘
src            └─┘  └────┘  └─────┘  └┘└────┘└──┘  
typ            └─┘└┘└────┘  └─────┘ └┘└────┘└──┘└┘
doc            └─┘  └────┘  └─────┘  └┘      └──┘  
txt            └─┘  └────┘  └─────┘  └┘      └──┘  
par            └─┘  └────┘  └─────┘  └┘      └──┘  
pid                └────┘          └┘      └──┘  
st   ─────────┘└─────────┘└────────────────────────┘└─
169            rw seq.destruct_eq_cons e,
id                └──────────────────┘ 
src            └─┘└──────────────────┘
typ            └─┘└──────────────────┘
doc            └─┘                    
txt            └─┘                    
par            └─┘                    
pid                                  
st   ──────────────────────────────────┘└─
170            apply seq.mem_cons },
id                   └──────────┘
src            └────┘└──────────┘
typ            └────┘└──────────┘
doc            └────┘            
txt            └────┘            
par            └────┘            
pid                             
st   ────────────────────────────┘└┘
171          { exact let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩ in ⟨c, or.inl cl, ac⟩ } },
id                          └┘  └┘     └──┘     └┘  └┘         └────┘
src            └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘└────┘  └┘  └┘
typ            └────┘    └┘└┘└┘└┘└───┘└──┘ └┘└┘└┘└┘└───┘  └┘└────┘  └┘  └┘
doc            └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  └┘
txt            └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  └┘
par            └────┘     └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  └┘
pid                      └┘  └┘  └───┘       └┘  └┘  └───┘  └┘        └┘  
st   ───────────────────────────────────────────────────────────────────────────┘└──┘
172        { refine ⟨d, or.inr _, ad⟩,
id                     └────┘    └┘
src          └─────┘  └┘└────┘└──┘  
typ          └─────┘ └┘└────┘└──┘└┘
doc          └─────┘  └┘      └──┘  
txt          └─────┘  └┘      └──┘  
par          └─────┘  └┘      └──┘  
pid                  └┘      └──┘  
st   ───────────────────────────────┘└─
173          rw seq.destruct_eq_cons e,
id              └──────────────────┘ 
src          └─┘└──────────────────┘
typ          └─┘└──────────────────┘
doc          └─┘                    
txt          └─┘                    
par          └─┘                    
pid                                
st   ────────────────────────────────┘└─
174          exact seq.mem_cons_of_mem _ dS' } } }
id                 └─────────────────┘   └─┘
src          └────┘└─────────────────┘└─┘   
typ          └────┘└─────────────────┘└─┘└─┘
doc          └────┘                   └─┘   
txt          └────┘                   └─┘   
par          └────┘                   └─┘   
pid                                  └─┘   
st   ───────────────────────────────────────┘└─────
175  end
st   ──┘
176  
177  theorem map_parallel (f : α → β) (S) : map f (parallel S) = parallel (S.map (map f)) :=
id                                        └─┘   └──────┘    └──────┘  └──┘  └─┘ 
src                                         └─┘    └──────┘     └──────┘   └──┘  └─┘
typ                                       └─┘   └──────┘    └──────┘  └──┘  └─┘ 
doc                                         └─┘    └──────┘      └──────┘   └──┘  └─┘
178  begin
st   └─────
179    refine eq_of_bisim (λ c1 c2, ∃ l S,
id            └─────────┘               
src    └─────┘└─────────┘  └──────┘└──┘
typ    └─────┘└─────────┘  └──────┘└──┘
doc    └─────┘             └──────┘ └──┘ 
txt    └─────┘             └──────┘ └──┘ 
par    └─────┘             └──────┘ └──┘ 
pid                       └──────┘ └──┘ 
st   ──────────────────────────────────────
180      c1 = map f (corec parallel.aux1 (l, S)) ∧
id                                             
src  ───┘                          └┘ └─┘
typ  ───┘                          └┘ └─┘
doc  ───┘                            └┘ └─┘ 
txt  ───┘                            └┘ └─┘ 
par  ───┘                            └┘ └─┘ 
pid  ───┘                            └┘ └─┘ 
st   ──────────────────────────────────────────────
181      c2 = corec parallel.aux1 (l.map (map f), S.map (map f))) _ ⟨[], S, rfl, rfl⟩,
id            └───┘ └───────────┘   └──┘           └──┘  └─┘                   └─┘
src  ───┘   └───┘└───────────┘  └──┘     └─┘ └──┘ └─┘ └────┘   └┘ └┘   └┘└─┘
typ  ───┘   └───┘└───────────┘  └──┘     └─┘ └──┘ └─┘└────┘   └┘└┘   └┘└─┘
doc  ───┘   └───┘                        └─┘ └──┘ └─┘ └────┘   └┘ └┘   └┘   
txt  ───┘                                └─┘          └────┘   └┘ └┘   └┘   
par  ───┘                                └─┘          └────┘   └┘ └┘   └┘   
pid  ───┘                                └─┘          └────┘   └┘ └┘   └┘   
st   ───────────────────────────────────────────────────────────────────────────────┘└─
182    intros c1 c2 h, exact match c1, c2, h with ._, ._, ⟨l, S, rfl, rfl⟩ := begin
id                                 └┘  └┘  
src    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
typ    └────────────┘  └────┘     └┘└┘└┘└┘└────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
doc    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
txt    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
par    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
pid          └──────┘              └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
st   ───────────────┘└───────────────────────────────────────────────────────┘└─────
183      clear _match,
src  ───┘└──────────┘└─
typ  ───┘└──────────┘└─
doc  ───┘└──────────┘└─
txt  ───┘└──────────┘└─
par  ───┘└──────────┘└─
pid  ──────────────────
st   ───────────────┘└─
184      have : parallel.aux2 (l.map (map f)) = lmap f (rmap (list.map (map f)) (parallel.aux2 l)),
id                             └───┘            └──┘    └──┘  └──────┘  └─┘     └───────────┘ 
src  ───┘└─────┘              └───┘     └─┘ └──┘  └──┘ └──────┘ └─┘ └─┘ └───────────┘ └┘└─
typ  ───┘└─────┘              └───┘     └─┘ └──┘  └──┘ └──────┘ └─┘└─┘ └───────────┘└┘└─
doc  ───┘└─────┘                        └─┘ └──┘  └──┘          └─┘ └─┘               └┘└─
txt  ───┘└─────┘                        └─┘                         └─┘               └┘└─
par  ───┘└─────┘                        └─┘                         └─┘               └┘└─
pid  ──────────┘                        └─┘                         └─┘               └───
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
185      { simp [parallel.aux2],
id               └───────────┘
src  ─────┘└────┘└───────────┘└─
typ  ─────┘└────┘└───────────┘└─
doc  ─────┘└────┘             └─
txt  ─────┘└────┘             └─
par  ─────┘└────┘             └─
pid  ───────────┘             └──
st   ────┘└───────────────────┘└─
186        induction l with c l IH; simp, rw [IH],
id                                           └┘
src  ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘  └─
typ  ─────┘└────────┘└──────────┘└┘└──┘└┘└──┘└┘└─
doc  ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘  └─
txt  ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘  └─
par  ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘  └─
pid  ───────────────┘ └──────────────────────┘  └──
st   ──────────────────────────────────┘└──────┘└─
187        cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l; simp [parallel.aux2],
id               └────────┘ └────────────────────┘  └─────┘ └──────┘          └───────────┘
src  ─────┘└────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘ └┘└────┘└───────────┘└─
typ  ─────┘└────┘└────────┘└────────────────────┘ └─────┘└──────┘└┘└┘└────┘└───────────┘└─
doc  ─────┘└────┘                                                └┘ └┘└────┘             └─
txt  ─────┘└────┘                                                └┘ └┘└────┘             └─
par  ─────┘└────┘                                                └┘ └┘└────┘             └─
pid  ───────────┘                                                └┘ └──────┘             └──
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
188        cases destruct c; simp },
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└───┘└──
typ  ─────┘└────┘└──────┘└┘└───┘└──
doc  ─────┘└────┘└──────┘ └┘└───┘└──
txt  ─────┘└────┘         └┘└───┘└──
par  ─────┘└────┘         └┘└───┘└──
pid  ───────────┘         └─────────
st   ────────────────────────────┘└─
189      simp [parallel.aux1], rw this, cases parallel.aux2 l with a l'; simp,
id             └───────────┘      └──┘        └───────────┘ 
src  ───┘└────┘└───────────┘└┘└─┘    └┘└────┘└───────────┘ └────────┘└┘└──┘└─
typ  ───┘└────┘└───────────┘└┘└─┘└──┘└┘└────┘└───────────┘└────────┘└┘└──┘└─
doc  ───┘└────┘             └┘└─┘    └┘└────┘              └────────┘└┘└──┘└─
txt  ───┘└────┘             └┘└─┘    └┘└────┘              └────────┘└┘└──┘└─
par  ───┘└────┘             └┘└─┘    └┘└────┘              └────────┘└┘└──┘└─
pid  ─────────┘             └────┘    └──────┘              └─────────────────
st   ───────────────────────┘└───────┘└─────────────────────────────────────┘└─
190      apply S.cases_on _ (λ c S, _) (λ S, _); simp; simp [parallel.aux1];
id             └────────┘                                    └───────────┘
src  ───┘└────┘└────────┘└─┘  └───────┘  └────┘└┘└──┘└┘└────┘└───────────┘└─
typ  ─────────┘└────────┘└─┘  └───────┘  └──────┘└──┘└┘└────┘└───────────┘└─
doc  ───┘└────┘          └─┘  └───────┘  └────┘└┘└──┘└┘└────┘             └─
txt  ───┘└────┘          └─┘  └───────┘  └────┘└┘└──┘└┘└────┘             └─
par  ─────────┘          └─┘  └───────┘  └──────┘└──┘└┘└────┘             └─
pid  ─────────┘          └─┘  └───────┘  └──────────────────┘             └──
st   ────────────────────────────────────────────────────────────────────────
191      exact ⟨_, _, rfl, rfl⟩
id                         └─┘
src  ─────────┘ └────┘   └┘└─┘└─
typ  ─────────┘ └────┘   └┘└─┘└─
doc  ─────────┘ └────┘   └┘   └─
txt  ─────────┘ └────┘   └┘   └─
par  ─────────┘ └────┘   └┘   └─
pid  ─────────┘ └────┘   └┘   └─
st   ───────────────────────────
192    end end
src  ─────────┘
typ  ─────────┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ────────┘
st   ─┘└─┘└───┘
193  end
st   └─┘
194  
195  theorem parallel_empty (S : wseq (computation α)) (h : S.head ~> none) :
id                               └──┘  └─────────┘         └───┘ └┘ └──┘
src                              └──┘  └─────────┘           └───┘ └┘ └──┘
typ                              └──┘  └─────────┘         └───┘ └┘ └──┘
doc                              └──┘  └─────────┘           └───┘ └┘
196  parallel S = empty _ :=
id   └──────┘   └───┘
src  └──────┘    └───┘
typ  └──────┘   └───┘
doc  └──────┘     └───┘
197  eq_empty_of_not_terminates $ λ ⟨a, m⟩,
id   └────────────────────────┘        
src  └────────────────────────┘
typ  └────────────────────────┘        
198  let ⟨c, cs, ac⟩ := exists_of_mem_parallel m,
id   └─┘     └┘         └────────────────────┘
src                     └────────────────────┘
typ  └─┘     └┘         └────────────────────┘
199      ⟨n, nm⟩ := exists_nth_of_mem cs,
id           └┘     └───────────────┘
src                 └───────────────┘
typ          └┘     └───────────────┘
200      ⟨c', h'⟩ := head_some_of_nth_some nm in by injection h h'
id                   └───────────────────┘                     └┘
src                  └───────────────────┘          └────────┘   
typ                  └───────────────────┘          └────────┘└┘
doc                                                 └────────┘   
txt                                                 └────────┘   
par                                                 └────────┘   
pid                                                             
st                                                 └───────────────
201  
src  
typ  
doc  
txt  
par  
pid  
st   
202  -- The reason this isn't trivial from exists_of_mem_parallel is because it eliminates to Sort
src  ─────────────────────────────────────────────────────────────────────────────────────────────┘
typ  ─────────────────────────────────────────────────────────────────────────────────────────────┘
doc  ─────────────────────────────────────────────────────────────────────────────────────────────┘
txt  ─────────────────────────────────────────────────────────────────────────────────────────────┘
par  ─────────────────────────────────────────────────────────────────────────────────────────────┘
pid  ─────────────────────────────────────────────────────────────────────────────────────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘
203  def parallel_rec {S : wseq (computation α)} (C : α → Sort v)
id                         └──┘  └─────────┘         
src                        └──┘  └─────────┘
typ                        └──┘  └─────────┘         
doc                        └──┘  └─────────┘
204    (H : ∀ s ∈ S, ∀ a ∈ s, C a) {a} (h : a ∈ parallel S) : C a :=
id                                      └──────┘      
src                                           └──────┘
typ                                     └──────┘      
doc                                             └──────┘
205  begin
st   └─────
206    let T : wseq (computation (α × computation α)) :=
id             └──┘                  └─────────┘ 
src    └──────┘└──┘              └─────────┘ └─────
typ    └──────┘└──┘              └─────────┘└─────
doc    └──────┘└──┘               └─────────┘ └─────
txt    └──────┘                               └─────
par    └──────┘                               └─────
pid    └───┘└─┘                               └┘└───
st   ────────────────────────────────────────────────────
207      S.map (λc, c.map (λ a, (a, c))),
id       └───┘       └──┘
src  ───┘└───┘  └─┘ └──┘  └──┘  └┘ └─┘
typ  ───┘└───┘  └─┘ └──┘  └──┘  └┘ └─┘
doc  ───┘└───┘  └─┘ └──┘  └──┘  └┘ └─┘
txt  ───┘       └─┘       └──┘  └┘ └─┘
par  ───┘       └─┘       └──┘  └┘ └─┘
pid  ───┘       └─┘       └──┘  └┘ └─┘
st   ──────────────────────────────────┘└─
208    have : S = T.map (map (λ c, c.1)),
id              └───┘  └─┘
src    └─────┘ └───┘ └─┘  └──┘ └──┘
typ    └─────┘└───┘ └─┘  └──┘ └──┘
doc    └─────┘  └───┘ └─┘  └──┘ └──┘
txt    └─────┘             └──┘ └──┘
par    └─────┘             └──┘ └──┘
pid    └───┘└┘             └──┘ └──┘
st   ──────────────────────────────────┘└─
209    { rw [←wseq.map_comp], refine (wseq.map_id _).symm.trans (congr_arg (λ f, wseq.map f S) _),
id            └───────────┘           └─────────┘                └───────┘       └──────┘   
src      └───┘└───────────┘  └─────┘ └─────────┘└─────────────┘ └───────┘  └──┘└──────┘  └──┘
typ      └───┘└───────────┘  └─────┘ └─────────┘└─────────────┘ └───────┘  └──┘└──────┘ └──┘
doc      └───┘               └─────┘            └─────────────┘            └──┘└──────┘  └──┘
txt      └───┘               └─────┘            └─────────────┘            └──┘          └──┘
par      └───┘               └─────┘            └─────────────┘            └──┘          └──┘
pid        └─┘                                 └─────────────┘            └──┘          └──┘
st   ───┘└────────────────┘└────────────────────────────────────────────────────────────────────┘└─
210      funext c, dsimp [id, function.comp], rw [←map_comp], exact (map_id _).symm },
id                        └┘  └───────────┘        └──────┘          └────┘
src      └──────┘  └─────┘└┘└┘└───────────┘  └───┘└──────┘  └────┘ └────┘└───────┘
typ      └──────┘  └─────┘└┘└┘└───────────┘  └───┘└──────┘  └────┘ └────┘└───────┘
doc      └──────┘  └─────┘  └┘               └───┘          └────┘       └───────┘
txt      └──────┘  └─────┘  └┘               └───┘          └────┘       └───────┘
par      └──────┘  └─────┘  └┘               └───┘          └────┘       └───────┘
pid            └┘         └┘                 └─┘                      └─────┘└┘
st   ───────────┘└─────────────────────────┘└─────────────┘└───────────────────────┘└┘
211    have pe := congr_arg parallel this, rw ←map_parallel at pe,
id                └───────┘ └──────┘ └──┘      └──────────┘
src    └─────────┘└───────┘└──────┘      └──┘└──────────┘└────┘
typ    └─────────┘└───────┘└──────┘└──┘  └──┘└──────────┘└────┘
doc    └─────────┘         └──────┘      └──┘            └────┘
txt    └─────────┘                       └──┘            └────┘
par    └─────────┘                       └──┘            └────┘
pid    └─────┘└─┘                         └┘            └────┘
st   ───────────────────────────────────┘└──────────────────────┘└─
212    have h' := h, rw pe at h',
id                     └┘
src    └─────────┘   └─┘  └────┘
typ    └─────────┘  └─┘└┘└────┘
doc    └─────────┘   └─┘  └────┘
txt    └─────────┘   └─┘  └────┘
par    └─────────┘   └─┘  └────┘
pid    └─────┘└─┘       └────┘
st   ─────────────┘└───────────┘└─
213    haveI : terminates (parallel T) := (terminates_map_iff _ _).1 ⟨_, h'⟩,
id             └────────┘  └──────┘       └────────────────┘            └┘
src    └──────┘└────────┘ └──────┘ └───┘ └────────────────┘└──────┘ └─┘  
typ    └──────┘└────────┘ └──────┘└───┘ └────────────────┘└──────┘ └─┘└┘
doc    └──────┘└────────┘ └──────┘ └───┘                   └──────┘ └─┘  
txt    └──────┘                    └───┘                   └──────┘ └─┘  
par    └──────┘                    └───┘                   └──────┘ └─┘  
pid         └┘                    └──┘                   └──────┘ └─┘  
st   ──────────────────────────────────────────────────────────────────────┘└─
214    induction e : get (parallel T) with a' c,
id                   └─┘  └──────┘ 
src    └────────┘ └─┘└─┘ └──────┘ └─────────┘
typ    └────────┘ └─┘└─┘ └──────┘└─────────┘
doc    └────────┘ └─┘└─┘ └──────┘ └─────────┘
txt    └────────┘ └─┘             └─────────┘
par    └────────┘ └─┘             └─────────┘
pid              └─┘             └───────┘
st   ─────────────────────────────────────────┘└─
215    have : a ∈ c ∧ c ∈ S,
id                    
src    └─────┘    
typ    └─────┘  
doc    └─────┘      
txt    └─────┘      
par    └─────┘      
pid    └───┘└┘      
st   ─────────────────────┘└─
216    { rcases exists_of_mem_map h' with ⟨d, dT, cd⟩,
id              └───────────────┘ └┘
src      └─────┘└───────────────┘  └───────────────┘
typ      └─────┘└───────────────┘└┘└───────────────┘
doc      └─────┘                   └───────────────┘
txt      └─────┘                   └───────────────┘
par      └─────┘                   └───────────────┘
pid                               └───────────────┘
st   ───┘└──────────────────────────────────────────┘└─
217      rw get_eq_of_mem _ dT at e, cases e, dsimp at cd, cases cd,
id          └───────────┘   └┘                                  └┘
src      └─┘└───────────┘└─┘  └───┘  └────┘   └─────────┘  └────┘
typ      └─┘└───────────┘└─┘└┘└───┘  └────┘  └─────────┘  └────┘└┘
doc      └─┘             └─┘  └───┘  └────┘   └─────────┘  └────┘
txt      └─┘             └─┘  └───┘  └────┘   └─────────┘  └────┘
par      └─┘             └─┘  └───┘  └────┘   └─────────┘  └────┘
pid                     └─┘  └───┘               └───┘       
st   ─────────────────────────────┘└───────┘└───────────┘└────────┘└─
218      rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩,
id              └────────────────────┘ └┘
src      └─────┘└────────────────────┘  └──────────────────┘
typ      └─────┘└────────────────────┘└┘└──────────────────┘
doc      └─────┘                        └──────────────────┘
txt      └─────┘                        └──────────────────┘
par      └─────┘                        └──────────────────┘
pid                                    └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
219      rcases wseq.exists_of_mem_map dT' with ⟨c', cs', e'⟩,
id              └────────────────────┘ └─┘
src      └─────┘└────────────────────┘   └─────────────────┘
typ      └─────┘└────────────────────┘└─┘└─────────────────┘
doc      └─────┘                         └─────────────────┘
txt      └─────┘                         └─────────────────┘
par      └─────┘                         └─────────────────┘
pid                                     └─────────────────┘
st   ───────────────────────────────────────────────────────┘└─
220      rw ←e' at ad',
id           └┘
src      └──┘  └─────┘
typ      └──┘└┘└─────┘
doc      └──┘  └─────┘
txt      └──┘  └─────┘
par      └──┘  └─────┘
pid        └┘  └─────┘
st   ────────────────┘└─
221      rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩, injection e' with i1 i2,
id              └───────────────┘ └─┘                               └┘
src      └─────┘└───────────────┘   └─────────────────┘  └────────┘  └─────────┘
typ      └─────┘└───────────────┘└─┘└─────────────────┘  └────────┘└┘└─────────┘
doc      └─────┘                    └─────────────────┘  └────────┘  └─────────┘
txt      └─────┘                    └─────────────────┘  └────────┘  └─────────┘
par      └─────┘                    └─────────────────┘  └────────┘  └─────────┘
pid                                └─────────────────┘             └─────────┘
st   ──────────────────────────────────────────────────┘└───────────────────────┘└─
222      constructor, rwa [i1, i2] at ac', rwa i2 at cs' },
id                         └┘  └┘              └┘
src      └─────────┘  └───┘  └┘  └──────┘  └──┘  └──────┘
typ      └─────────┘  └───┘└┘└┘└┘└──────┘  └──┘└┘└──────┘
doc      └─────────┘  └───┘  └┘  └──────┘  └──┘  └──────┘
txt      └─────────┘  └───┘  └┘  └──────┘  └──┘  └──────┘
par      └─────────┘  └───┘  └┘  └──────┘  └──┘  └──────┘
pid                      └┘  └┘  └─────┘       └─────┘
st   ──────────────┘└───────┘└──┘└─────┘└──────────────┘└┘
223    cases this with ac cs, apply H _ cs _ ac
id           └──┘                      └┘   └┘
src    └────┘    └─────────┘  └────┘ └─┘  └─┘  
typ    └────┘└──┘└─────────┘  └────┘└─┘└┘└─┘└┘
doc    └────┘    └─────────┘  └────┘ └─┘  └─┘  
txt    └────┘    └─────────┘  └────┘ └─┘  └─┘  
par    └────┘    └─────────┘  └────┘ └─┘  └─┘  
pid             └─────────┘        └─┘  └─┘  
st   ──────────────────────┘└──────────────────┘
224  end
st   └─┘
225  
226  theorem parallel_promises {S : wseq (computation α)} {a}
id                                  └──┘  └─────────┘ 
src                                 └──┘  └─────────┘
typ                                 └──┘  └─────────┘ 
doc                                 └──┘  └─────────┘
227    (H : ∀ s ∈ S, s ~> a) : parallel S ~> a :=
id                  └┘     └──────┘  └┘ 
src                    └┘      └──────┘   └┘
typ                 └┘     └──────┘  └┘ 
doc                    └┘      └──────┘   └┘
228  λ a' ma', let ⟨c, cs, ac⟩ := exists_of_mem_parallel ma' in H _ cs ac
id     └┘ └─┘  └─┘     └┘  └┘     └────────────────────┘ └─┘    
src                               └────────────────────┘
typ    └┘ └─┘  └─┘     └┘  └┘     └────────────────────┘ └─┘    
229  
230  theorem mem_parallel {S : wseq (computation α)} {a}
id                             └──┘  └─────────┘ 
src                            └──┘  └─────────┘
typ                            └──┘  └─────────┘ 
doc                            └──┘  └─────────┘
231    (H : ∀ s ∈ S, s ~> a) {c} (cs : c ∈ S) (ac : a ∈ c) : a ∈ parallel S :=
id                  └┘                               └──────┘ 
src                    └┘                                     └──────┘
typ                 └┘                               └──────┘ 
doc                    └┘                                        └──────┘
232  by haveI := terminates_of_mem ac; have := terminates_parallel cs;
id               └───────────────┘ └┘          └─────────────────┘ └┘
src     └───────┘└───────────────┘    └──────┘└─────────────────┘
typ     └───────┘└───────────────┘└┘  └──────┘└─────────────────┘└┘
doc     └───────┘                     └──────┘                   
txt     └───────┘                     └──────┘                   
par     └───────┘                     └──────┘                   
pid          └─┘                     └───┘└─┘                   
st     └───────────────────────────────────────────────────────────────
233     exact mem_of_promises _ (parallel_promises H)
id            └─────────────┘    └───────────────┘ 
src     └────┘└─────────────┘└─┘ └───────────────┘ └─
typ     └────┘└─────────────┘└─┘ └───────────────┘└─
doc     └────┘               └─┘                   └─
txt     └────┘               └─┘                   └─
par     └────┘               └─┘                   └─
pid                         └─┘                   
st   ─────────────────────────────────────────────────
234  
src  
typ  
doc  
txt  
par  
pid  
st   
235  theorem parallel_congr_lem {S T : wseq (computation α)} {a}
id                                     └──┘  └─────────┘ 
src                                    └──┘  └─────────┘
typ                                    └──┘  └─────────┘ 
doc                                    └──┘  └─────────┘
236    (H : S.lift_rel equiv T) : (∀ s ∈ S, s ~> a) ↔ (∀ t ∈ T, t ~> a) :=
id          └───────┘ └───┘              └┘             └┘ 
src          └───────┘ └───┘                  └┘                 └┘
typ         └───────┘ └───┘              └┘             └┘ 
doc          └───────┘ └───┘                  └┘                  └┘
237  ⟨λ h1 t tT, let ⟨s, sS, se⟩ := wseq.exists_of_lift_rel_right H tT in
id      └┘  └┘  └─┘     └┘  └┘     └───────────────────────────┘  └┘
src                                 └───────────────────────────┘
typ     └┘  └┘  └─┘     └┘  └┘     └───────────────────────────┘  └┘
238    (promises_congr se _).1 (h1 _ sS),
id      └────────────┘         └┘
src     └────────────┘      
typ     └────────────┘         └┘
239  λ h2 s sS, let ⟨t, tT, se⟩ := wseq.exists_of_lift_rel_left H sS in
id     └┘  └┘  └─┘     └┘  └┘     └──────────────────────────┘  └┘
src                                └──────────────────────────┘
typ    └┘  └┘  └─┘     └┘  └┘     └──────────────────────────┘  └┘
240    (promises_congr se _).2 (h2 _ tT)⟩
id      └────────────┘         └┘
src     └────────────┘      
typ     └────────────┘         └┘
241  
242  -- The parallel operation is only deterministic when all computation paths lead to the same value
243  theorem parallel_congr_left {S T : wseq (computation α)} {a}
id                                      └──┘  └─────────┘ 
src                                     └──┘  └─────────┘
typ                                     └──┘  └─────────┘ 
doc                                     └──┘  └─────────┘
244    (h1 : ∀ s ∈ S, s ~> a) (H : S.lift_rel equiv T) : parallel S ~ parallel T :=
id                   └┘        └───────┘ └───┘     └──────┘   └──────┘ 
src                     └┘          └───────┘ └───┘      └──────┘    └──────┘
typ                  └┘        └───────┘ └───┘     └──────┘   └──────┘ 
doc                     └┘          └───────┘ └───┘      └──────┘    └──────┘
245  let h2 := (parallel_congr_lem H).1 h1 in
id       └┘     └────────────────┘    └┘
src             └────────────────┘   
typ      └┘     └────────────────┘    └┘
246  λ a', ⟨λh, by have aa := parallel_promises h1 h; rw ←aa; rw ←aa at h; exact
id     └┘                    └───────────────┘ └┘       └┘      └┘
src                └─────────┘└───────────────┘     └──┘    └──┘  └───┘  └─────
typ    └┘         └─────────┘└───────────────┘└┘  └──┘└┘  └──┘└┘└───┘  └─────
doc                └─────────┘                      └──┘    └──┘  └───┘  └─────
txt                └─────────┘                      └──┘    └──┘  └───┘  └─────
par                └─────────┘                      └──┘    └──┘  └───┘  └─────
pid                └─────┘└─┘                        └┘      └┘  └───┘       
st                └──────────────────────────────────────────────────────────────
247    let ⟨s, sS, as⟩ := exists_of_mem_parallel h,
id             └┘  └┘     └────────────────────┘ 
src  ─┘     └┘  └┘  └───┘└────────────────────┘ └─
typ  ─┘     └┘└┘└┘└┘└───┘└────────────────────┘└─
doc  ─┘     └┘  └┘  └───┘                       └─
txt  ─┘     └┘  └┘  └───┘                       └─
par  ─┘     └┘  └┘  └───┘                       └─
pid  ─┘     └┘  └┘  └───┘                       └─
st   ───────────────────────────────────────────────
248        ⟨t, tT, st⟩ := wseq.exists_of_lift_rel_left H sS,
id             └┘  └┘     └──────────────────────────┘ 
src  ─────┘  └┘  └┘  └───┘└──────────────────────────┘   └─
typ  ─────┘  └┘└┘└┘└┘└───┘└──────────────────────────┘  └─
doc  ─────┘  └┘  └┘  └───┘                               └─
txt  ─────┘  └┘  └┘  └───┘                               └─
par  ─────┘  └┘  └┘  └───┘                               └─
pid  ─────┘  └┘  └┘  └───┘                               └─
st   ────────────────────────────────────────────────────────
249        aT := (st _).1 as in mem_parallel h2 tT aT,
id                              └──────────┘ └┘
src  ───────────┘   └────┘  └──┘└──────────┘    
typ  ───────────┘   └────┘  └──┘└──────────┘└┘  
doc  ───────────┘   └────┘  └──┘                
txt  ───────────┘   └────┘  └──┘                
par  ───────────┘   └────┘  └──┘                
pid  ───────────┘   └────┘  └──┘                
st   ───────────────────────────────────────────────┘
250  λh, by have aa := parallel_promises h2 h; rw ←aa; rw ←aa at h; exact
id                    └───────────────┘ └┘       └┘      └┘
src         └─────────┘└───────────────┘     └──┘    └──┘  └───┘  └─────
typ        └─────────┘└───────────────┘└┘  └──┘└┘  └──┘└┘└───┘  └─────
doc         └─────────┘                      └──┘    └──┘  └───┘  └─────
txt         └─────────┘                      └──┘    └──┘  └───┘  └─────
par         └─────────┘                      └──┘    └──┘  └───┘  └─────
pid         └─────┘└─┘                        └┘      └┘  └───┘       
st         └──────────────────────────────────────────────────────────────
251    let ⟨s, sS, as⟩ := exists_of_mem_parallel h,
id             └┘  └┘     └────────────────────┘ 
src  ─┘     └┘  └┘  └───┘└────────────────────┘ └─
typ  ─┘     └┘└┘└┘└┘└───┘└────────────────────┘└─
doc  ─┘     └┘  └┘  └───┘                       └─
txt  ─┘     └┘  └┘  └───┘                       └─
par  ─┘     └┘  └┘  └───┘                       └─
pid  ─┘     └┘  └┘  └───┘                       └─
st   ───────────────────────────────────────────────
252        ⟨t, tT, st⟩ := wseq.exists_of_lift_rel_right H sS,
id             └┘  └┘     └───────────────────────────┘ 
src  ─────┘  └┘  └┘  └───┘└───────────────────────────┘   └─
typ  ─────┘  └┘└┘└┘└┘└───┘└───────────────────────────┘  └─
doc  ─────┘  └┘  └┘  └───┘                                └─
txt  ─────┘  └┘  └┘  └───┘                                └─
par  ─────┘  └┘  └┘  └───┘                                └─
pid  ─────┘  └┘  └┘  └───┘                                └─
st   ─────────────────────────────────────────────────────────
253        aT := (st _).2 as in mem_parallel h1 tT aT⟩
id                              └──────────┘ └┘
src  ───────────┘   └────┘  └──┘└──────────┘    
typ  ───────────┘   └────┘  └──┘└──────────┘└┘  
doc  ───────────┘   └────┘  └──┘                
txt  ───────────┘   └────┘  └──┘                
par  ───────────┘   └────┘  └──┘                
pid  ───────────┘   └────┘  └──┘                
st   ───────────────────────────────────────────────┘
254  
255  theorem parallel_congr_right {S T : wseq (computation α)} {a}
id                                       └──┘  └─────────┘ 
src                                      └──┘  └─────────┘
typ                                      └──┘  └─────────┘ 
doc                                      └──┘  └─────────┘
256    (h2 : ∀ t ∈ T, t ~> a) (H : S.lift_rel equiv T) : parallel S ~ parallel T :=
id                   └┘        └───────┘ └───┘     └──────┘   └──────┘ 
src                     └┘          └───────┘ └───┘      └──────┘    └──────┘
typ                  └┘        └───────┘ └───┘     └──────┘   └──────┘ 
doc                     └┘          └───────┘ └───┘      └──────┘    └──────┘
257  parallel_congr_left ((parallel_congr_lem H).2 h2) H
id   └─────────────────┘   └────────────────┘    └┘  
src  └─────────────────┘   └────────────────┘   
typ  └─────────────────┘   └────────────────┘    └┘  
258  
259  end computation